left, right:Realizer. (left  right)  Realizer 

latex

Definitions	x:A. B(x), Realizer, t  T, left  right, Prop, x. t(x), x(s)
Lemmas	Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, unit wf